\begin{tabbing}
sendMinimalR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $d_{1}$; $d_{2}$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=weakSendDoApplyR\=\{\$a:ut2, \$tg:ut2\}\+\+
\\[0ex]($T$; $t$; $l$; ${\it ds}_{1}$; $f$ o' mu'($\lambda$$s$,$n$. $\neg_{b}$($P$($s$,$n$)))); 
\\[0ex]
\-\\[0ex]weakSendDoApplyR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($\mathbb{N}$; 0; lnk{-}inv($l$); ${\it ds}_{2}$; mu'($\lambda$$s$,$n$. $\neg_{b}$($Q$($s$,$n$))))])
\-\-
\end{tabbing}